Independence-friendly logic (IF logic), proposed by Jaakko Hintikka and Gabriel Sandu, aims at being a more natural and intuitive alternative to classical first-order logic (FOL). IF logic is characterized by branching quantifiers. It is more expressive than FOL because it allows one to express independence relations between quantified variables.
For example, the formula ∀a ∀b ∃c/b ∃d/a φ(a,b,c,d) ("x/y" should be read as "x independent of y") cannot be expressed in FOL. This is because c depends only on a and d depends only on b. First-order logic cannot express these independences by any linear reordering of the quantifiers.
Contents |
Since Tarskian semantics does not allow indeterminate truth values, it cannot be used for IF logic. Hintikka further argues that the standard semantics of FOL cannot accommodate IF logic because the principle of compositionality fails in the latter. Wilfrid Hodges (1997) gives a compositional semantics for it in part by having the truth clauses for IF formulas quantify over sets of assignments rather than just assignments (as the usual truth clauses do).
The game-theoretic semantics for FOL treats a FOL formula as a game of perfect information, whose players are Verifier and Falsifier. The same holds for the standard semantics of IF logic, except that the games are of imperfect information.
Independence relations between the quantified variables are modelled in the game tree as indistinguishability relations between game states with respect to a certain player. In other words, the players are not certain where they are in the tree (this ignorance simulates simultaneous play). The formula is evaluated as true if there Verifier has a winning strategy, false if Falsifier has a winning strategy, and indeterminate otherwise.
A winning strategy is informally defined as a strategy that is guaranteed to win the game, regardless of how the other players play. It can be given a completely rigorous, formal definition.
Feferman (2006) cites a theorem of Väänänen which states that "the general question of validity of IF sentences is recursively isomorphic to that for validity in full second-order logic". He argues (contra Hintikka) that while satisfiability might be a first-order matter, the question of whether there is a winning strategy for Verifier over all structures in general "lands us squarely in full second order logic" (emphasis Feferman's).